Nuprl Lemma : fseg_member
11,40
postcript
pdf
T
:Type,
l1
,
l2
:(
T
List),
x
:
T
. fseg(
T
;
l1
;
l2
)
(
x
l1
)
(
x
l2
)
latex
ProofTree
Definitions
{
T
}
,
(
x
l
)
,
P
Q
,
x
:
A
B
(
x
)
,
P
Q
,
P
Q
,
x
:
A
B
(
x
)
,
P
&
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
Type
,
,
t
T
,
s
=
t
,
{
x
:
A
|
B
(
x
)}
,
,
s
~
t
,
type
List
,
SQType(
T
)
,
[
car
/
cdr
]
,
A
B
,
i
j
,
||
as
||
,
x
:
A
.
B
(
x
)
,
fseg(
T
;
L1
;
L2
)
Lemmas
fseg
wf
,
non
neg
length
,
cons
one
one
,
guard
wf
,
nat
wf
,
member
wf
,
member
append
,
l
member
wf
origin
T:Type, l1, l2:(T List), x:T. fseg(T;l1;l2) 
(x 
l1) (x l2)
T:Type, l1, l2:(T List), x:T. fseg(T;l1;l2) (x l1) (x l2)
l)
Q
B(x) Q
Q
B(x) Qx:A. B(x)
T
B
j 
x:A. B(x)